/*
 * To change this license header, choose License Headers in Project Properties.
 * To change this template file, choose Tools | Templates
 * and open the template in the editor.
 */
package tp2ia_partie2;

import java.util.LinkedHashSet;
import java.util.ArrayList;
import java.util.Set;
import tp2ia_partie2.objects.Clause;
import tp2ia_partie2.objects.Litteral;

/**
 *
 * @author hp
 */

public class Resolution_1 {

    /*
     function PL-RESOLUTION(KB,α) returns true or false
     inputs: KB, the knowledge base, a sentence α in propositional logic, the query, a
     sentence in propositional logic 
     clauses <--- the set of clauses in the CNF representation of KB ∧ ¬α
     new <--- {}
     loop do
     for each Ci, Cj in clauses do
     resolvents <----- PL-RESOLVE(Ci, Cj)
     if resolvents contains the empty clause then return true
     new <--- new ∪ resolvents
     if new ⊆ clauses then return false
     clauses <---- clauses  ∪ new   
     */
    public boolean plResolution(Set<Clause> KB, Clause alpha) {

        // clauses <--- the set of clauses in the CNF representation of KB ∧ ¬α
        Set<Clause> clauses = KB;
        clauses.add(alpha);
        clauses = transformToSimpleClauses(clauses);
        //new <--- {}
        Set<Clause> newClauses = new LinkedHashSet<Clause>();
        //loop do
        do { 
            System.out.println("\n---- Iteration ----");
            //for each Ci, Cj in clauses do
            for (int i = 0; i < clauses.size() - 1; i++) {
                Clause ci = new ArrayList<Clause>(clauses).get(i);
                for (int j = i + 1; j < clauses.size(); j++) {
                    Clause cj = new ArrayList<Clause>(clauses).get(j);
                    System.out.println("-->Appel de plResolve(" + ci + "," + cj + ")");
                    // resolvents <- PL-RESOLVE(C_i, C_j)
                    Set<Clause> resolvents = plResolve(ci, cj);
                    // if resolvents contains the empty clause then return true
                    if (resolvents == null) {
                        return true;
                    }
                    // new <- new union resolvents
                    newClauses.addAll(resolvents);
                    
                }
            }
            // if new is subset of clauses then return false
            if (clauses.containsAll(newClauses)) {
                System.out.println("\t--> Aucune nouvelle clause trouvée");
                return false;
            }
            // clauses <- clauses union new
            clauses.addAll(newClauses);
        } while (true);
    }

    private Set<Clause> plResolve(Clause ci, Clause cj) {

        boolean resolution = false;

        Set<Litteral> ciLitteraux = ci.getLitteraux();
        Set<Litteral> cjLitteraux = cj.getLitteraux();

        for (Litteral li : ciLitteraux) {
            for (Litteral lj : cjLitteraux) {

                if (li.estActive() && lj.estActive()) {
                    if (li.getC().equals(lj.getC()) && (li.isNegation() != lj.isNegation())) {
                        System.out.println("\t--> Deux littereaux complimentaires trouvés " + li.getC()+ " et ¬"+ li.getC());
                        li.desactiver();
                        lj.desactiver();
                        resolution = true;
                    }
                }
            }
        }
        if (!resolution) {
            // retourner les 2 clause
            Set<Clause> result = new LinkedHashSet<Clause>();
            result.add(ci);
            result.add(cj);
            return result;
        } else {
            // creer des nouveaux clause en eliminant les littereaux desactivés
            Set<Clause> result = new LinkedHashSet<Clause>();
            if (ci.getActiveLitteraux() != null) {
                result.add(ci.getActiveLitteraux());
            }
            if (cj.getActiveLitteraux() != null) {
                result.add(cj.getActiveLitteraux());
            }
            if (result.size() == 0) {
                return null;
            }
            return result;
        }
    }
    
    private Set<Clause> transformToSimpleClauses(Set<Clause> clauses) {

        Set<Clause> simpleClauses = new LinkedHashSet<Clause>();
        for (Clause c : clauses) {
            simpleClauses.add(c.toSimpleClause());
        }
        return simpleClauses;
    }

}
